home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
Language/OS - Multiplatform Resource Library
/
LANGUAGE OS.iso
/
quintus
/
quintus0.lha
/
work
/
csplit_2.05.4
< prev
next >
Wrap
Text File
|
1992-04-03
|
3KB
|
129 lines
%%%
%%% version 2.05.1
%%% initial version
%%% split horn clauses into horn clauses
%%% version 2.05.4
%%% saved split clauses as sent_c
%%%
%%% This is the code for clause splitting.
%%%
%%%
%%% Split_clauses splits clauses when necessary.
%%%
split_clauses :-
clause_splitting(N),
sent_C(cl(CSize,_,by(C,V,V,V1,_),I,sp(S,_,_),_,_,_,_)),
length(C,N1),
N1 > N,
erase_clause_C(CSize,C,V1),
split_clause(C,N,Cs),
assert_split_clause(Cs,I,S),
print_split_clause(C,Cs),
fail.
split_clauses :-
sentc_to_sentC_z,
!.
%%%
%%% Split_clause splits a single clause.
%%%
split_clause(C,N,[C]) :-
length(C,N1),
N1 =< N,
!.
split_clause(C,N,[C3|Cs]) :-
N1 is N - 1,
split_clause_1(C,N1,C1,C2),
common_variables(C1,C2,Xs),
gensym('cs$',F),
L=..[F|Xs],
split_clause_3(C1,C2,L,C3,C4),
!,
split_clause(C4,N,Cs).
split_clause_1(C,N,C1,C2) :-
split_clause_2(C,N,C1,C2,1),
!.
split_clause_2([L|Ls],N,[L],Ls,N).
split_clause_2([L|Ls],N,[L|C1],C2,N1) :-
N2 is N1 + 1,
!,
split_clause_2(Ls,N,C1,C2,N2).
split_clause_3(C1,C2,L,[not L|C1],[L|C2]) :-
split_clause_4(C1),
!.
split_clause_3(C1,C2,L,[L|C1],[not L|C2]).
split_clause_4([not _|Ls]) :-
!,
split_clause_4(Ls).
split_clause_4([_|Ls]) :-
negclause(Ls),
!.
%%%
%%% Assert_split_clause asserts the clauses obtained from splitting a clause.
%%% Note that none of clauses to be asserted can be a duplicate of an existing
%%% clauses since they contain a unique literal. Thus, no duplicate checking
%%% is done.
%%%
assert_split_clause([],_,_).
assert_split_clause([C|Cs],I,S) :-
assert_split_clause_1(C,I,S),
!,
assert_split_clause(Cs,I,S).
assert_split_clause_1(C,I,S) :-
vars_tail(C,V),
clause_size(C,CSize),
linearize_term(C,C1,V1,V2),
vars_literals(C,W),
compute_V_lits(W,0,NLits),
set_sr_status(S,C1,Sp,Ds),
list_of_Ns(C1,0,Dis),
calculate_priority_clause(C1,Sp,Ds,Pr),
assert_split_clause_2(Pr),
assertz(sent_c(cl(CSize,NLits,by(C1,V1,V2,V,W),I,Sp,Ds,0,Dis,Pr))),
!.
assert_split_clause_2(Pr) :-
priority_bound(PrioBound),
!,
check_prioritybound(Pr,PrioBound),
!.
assert_split_clause_2(_).
%%%
%%% Print_split_clause prints the result of splitting a clause.
%%%
print_split_clause(_,_) :-
not(outcsplit),
!.
print_split_clause(C,Cs) :-
nl,
write_line(5,'clause split:'),
not(not(print_split_clause_1(C,Cs))),
!.
print_split_clause_1(C,Cs) :-
vars_tail(C,V),
var_list(V),
write_line(10,'orig: ',C),
print_split_clause_2(Cs),
!.
print_split_clause_2([C|Cs]) :-
print_split_clause_4(C),
!,
print_split_clause_3(Cs).
print_split_clause_3([]).
print_split_clause_3([C|Cs]) :-
print_split_clause_5(C),
!,
print_split_clause_3(Cs).
print_split_clause_4(C) :-
vars_tail(C,V),
var_list(V),
write_line(10,'split: ',C),
!.
print_split_clause_5(C) :-
vars_tail(C,V),
var_list(V),
write_line(10,' : ',C),
!.